package org.eclipse.iota.rules;

import static org.eclipse.iota.model.EquationType.EQUAL;
import static org.eclipse.iota.model.EquationType.GREATER;
import static org.eclipse.iota.model.EquationType.LESS;

import org.eclipse.iota.model.Boolean;
import org.eclipse.iota.model.Clause;
import org.eclipse.iota.model.Equation;
import org.eclipse.iota.model.EquationType;
import org.eclipse.iota.model.Expression;
import org.eclipse.iota.monotonicity.IotaMonotonicityCalculator;
import org.eclipse.iota.monotonicity.Monotonicity;
import org.eclipse.iota.rewrite.AbstractIotaRule;
import org.eclipse.iota.util.IotaCopyUtil;

/**
 * @deprecated
 * @author Christian Krause
 * @generated NOT
 */
public class CheckMonotonicity extends AbstractIotaRule {
	
	/*
	 * (non-Javadoc)
	 * @see org.eclipse.iota.rules.AbstractIotaRule#visit(org.eclipse.iota.core.Equation)
	 */
	public void visit(Equation equation) {
		
		// Compute monotonicity:
		Boolean result = checkMonotonicity(equation);
		if (result==null) {
			Equation flipped = IotaCopyUtil.copy(equation);
			flipped.flip();
			result = checkMonotonicity(flipped);
		}
		
		// Successful?
		if (result!=null) {
			replaceEquation(equation, result);
		}
		
	}
	
	/*
	 * Helper method: check monotonicity (not symmetric)
	 */
	private Boolean checkMonotonicity(Equation equation) {
		
		// E.g. x < f(x)
		Expression argument = equation.getLeft();
		Expression target = equation.getRight();
		
		// Compute monotonicity:
		Monotonicity monotonicity = null; //IotaMonotonicityUtil.compute(target, argument, equation.getClause());
		if (monotonicity!=null) {
			
			// Get the equation type:
			EquationType type = equation.getType();
			/*
			switch (monotonicity) {
			
			case IDENTITY: return new Boolean(type==EQUAL);
			
			case STRICTLY_INCREASING: return new Boolean(type==GREATER);
			case STRICTLY_DECREASING: return new Boolean(type==LESS);
			
			case INCREASING: return new Boolean(type==EQUAL || type==GREATER);
			case DECREASING: return new Boolean(type==EQUAL || type==LESS);
			
			}
			*/
			
		}
		
		// No result:
		return null;
		
	}
	
	/*
	 * Helper method: replace an equation by a boolean and cleanup all booleans.
	 */
	private void replaceEquation(Equation equation, Boolean bool) {
		
		// Replace the equation:
		Clause clause = equation.getClause();
		int index = clause.getConstraints().indexOf(equation);
		clause.getConstraints().set(index, bool);
		
		// Simplify all booleans:
		//applyExternalRule(SimplifyPredicate.class);

	}
	
}
